(set-logic QF_BV)
(set-info :source |
 Patrice Godefroid, SAGE (systematic dynamic test generation)
 For more information: http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun T4_180 () (_ BitVec 32))
(declare-fun T1_180 () (_ BitVec 8))
(declare-fun T1_181 () (_ BitVec 8))
(declare-fun T1_182 () (_ BitVec 8))
(declare-fun T1_183 () (_ BitVec 8))
(assert (and true (= T4_180 (bvor (bvshl (bvor (bvshl (bvor (bvshl ((_ zero_extend 24) T1_183) (_ bv8 32)) ((_ zero_extend 24) T1_182)) (_ bv8 32)) ((_ zero_extend 24) T1_181)) (_ bv8 32)) ((_ zero_extend 24) T1_180))) (= T4_180 (_ bv2147483648 32)) (bvsle (_ bv0 32) T4_180) (not (= T4_180 (_ bv0 32)))))
(check-sat)
(exit)
